Design verification is increasingly recognized as a bottleneck in the design cycle. Formal verification allows finding design bugs in the early stages of design. Preferably, the formal verification is capable of fully proving the correctness of the design.
A Boolean decision procedure is found at the core of most verification algorithms. The most scalable and fastest among Boolean decision procedures are so-called satisfiability checking (or SAT) algorithms.
A classical satisfiability algorithm, known as a DPLL algorithm (short for the Davis-Putnam-Logemann-Loveland algorithm), takes as input a Boolean formula, f, and decides whether there is a truth assignment to variables of f that makes f evaluate to true. The formula, f, is represented in a special form, known as conjunctive normal form, or CNF.
A system under test, such as hardware, is in transition over time. The transition system is assumed to have an initial state corresponding to time zero. At every interval, such as a clock tick, the state of the system changes according to a transition relation. The state change describes how the system transitions from state to state.
The transition system may thus be characterized as having a set of states, a sub-set of initial states, and a transition relation. The transition relation determines how the transition system may transit from one state to the next, and may be characterized mathematically as a set of state pairs, for example, (s1, s2). The initial state relation defines what states the transition system may be in at time zero. In the transition systems discussed herein, states are given as truth assignments to a fixed number of Boolean variables (these Boolean variables represent the state elements of the hardware). The terms “transition system” and “finite state machine” (or FSM) are used herein interchangeably.
Bounded model checking (BMC) is a SAT-based verification technique used for finding counter-examples (CE) to a given safety property in a transition system. A safety property is a particular Boolean formula, P, in the system that is supposed to be true for all possible scenarios of the system. For a given transition system, C, a safety property, P, is valid if, for all reachable states, s, of the system, C, s(P)=true. Here, the reachable states of the system are the states into which the transition system can transition (from an initial state) in zero or more steps. (The safety properties discussed herein are limited to properties known as invariants.)
The idea of BMC is to unroll the transition system to k time steps, and search using a SAT solver for a state transition path of length less or equal to k, starting with an initial state and ending in a state violating the property. “Unrolling the transition system to k time steps” refers to obtaining a description of the system from time zero to time, k, in other words, building a sequence of states, s0, s1, sk, where state, sl, describes the transition system at time, l. The sequence s0, . . . , sk is referred to herein as a state transition path of the transition system. The methods described herein are designed to analyze state transition paths.
A SAT solver searches for a satisfying assignment to a Boolean formula written in conjunctive normal form (CNF). A CNF formula is represented as a set of clauses, a clause being a disjunction of literals, where a literal is a Boolean variable or its negation. A SAT problem may be represented using n variables, x1, x2, . . . , xn, which may be assigned truth values, 0 (false) or 1 (true). A literal is a variable, xl, or its negation, xl.
The CNF formula operated upon by the SAT solver is known as a SAT instance or a CNF instance. The SAT solver looks for a satisfying assignment of the SAT instance.
Proving a safety property, P, using the BMC technique means showing that there is no counter-example (CE) to P of a length less than or equal to the diameter of the system, i.e., the maximum length of a shortest (thus loop-free) path between any two states.
Practically speaking, BMC is an incomplete technique. BMC is rarely capable of proving a property arising from an industrial application of software or hardware verification. This is because the diameter for such systems is too large to handle by current SAT solvers. One solution to the BMC problem is a technique employing temporal induction.
A temporal induction algorithm proposes unrolling the transition system to depths lower than the diameter of the system. Roughly, BMC in the algorithm corresponds to the base of induction. The induction step, at depth m, attempts to prove that there is no state transition path, s0, . . . ,sm,sm+1 such that P holds in all but the last state (s0 need not be an initial state). Once such a depth, m, is found, and it has been shown in the base of induction that there is no counter-example, CE, to the property of length m or less, the property P is proven valid at all states reachable from the initial stats.
In a BMC run, to avoid unnecessary unrolling of the transition relation, one starts with low bounds, k, if no counter-example, CE, is found for the property of length smaller than or equal to k, the bound, k, is increased, repeatedly, until k reaches the diameter of the transition system, A BMC run thus involves a number of calls to the SAT solver. Similarly, proving the induction step in the algorithm involves several calls to the SAT solver, one for each increase of k as k approaches m. The distinct calls to the SAT solver are closely related.